COM: fun_1_summary

COM: fun_1_intro

ABS: Id

STM: identity wf

ABS: Id{T}

STM: tidentity wf

STM: my tidentity wf

STM: eta conv

ABS: x:T. b(x)

ABS: f o g

STM: compose wf

STM: comb for compose wf

STM: comp assoc

STM: comp id l

STM: comp id r

ABS: InvFuns(A;B;f;g)

STM: inv funs wf

STM: sq stable inv funs

ABS: 1-1-Corresp(A;B)

STM: one one corr wf

ABS: Inj(A;B;f)

STM: inject wf

STM: sq stable inject

ABS: Surj(A;B;f)

STM: surject wf

ABS: Bij(A;B;f)

STM: biject wf

STM: ax choice

STM: dep ax choice

STM: inv funs sym

STM: bij imp exists inv

STM: fun with inv is bij

STM: bij iff 1 1 corr

COM: fun_1_end

Up	Standard, Standard